Erlang with Types

Все знают что в Эрланге нет нормальной системы типов. По сути эрланг -- это
статически типизированный язык с одним тегированным типом оберткой, который
может включать фиксированный набор форматов. Такое вцелом называется
динамической типизацией, но в целом система типов (форматов) фиксированная.
Благодаря чему можно написать проверку входных и выходных параметров функций
(Dializer) чем можно сэкономить время при рефакторинге. Но если модуль
вызывается как Var:func, то проверку уже такую не сделать, а отсуствие вывода
типов влечет за собой прописывание всех возможных спецификаций которые можно
поставить только на вызовы функций.

Что бы прикинуть как мог бы выглядеть недо-типизированный Эрланг в классической
среде полиморфных типов лямбда-исчисления второго порядка ФСИСТЕМЕ! я накидал
этот документ который доступен на гитхабе: https://github.com/5HT/et

Типы

Первое чем я ограничился это синтаксисом Эрланга и Диалайзера. А также взял за
основу классическую систему типов ML. Функции над значениями и над типами
отличаются в ML-подобных языках. Вот какие типы конструкторов типов бывают:

fun(A,B,...) -> A -> B -> C ...
product(A,B,...) -> {A,B,...}
sum(A,B,...) -> A | B | ...
cat(A,B,...) -> Domains(A,B,...), Morphisms(A,B,...) end.

Где A,B,... -- конструкторы типов.

Конструкторы Типов

Конструкторы типов являются функциями на типах, с помощью которых мы
конструтируем другие типы. Если у конструктора нет параметров -- это означает
конкретный тип, который уже готовый к использования в функциях. Например
привычные для пользователей Erlang встроенные конкретные типы:

string() = list(char) = string/0.
integer().
atom().

В терминах теории категорий программа на типизированном языке представляет
собой ориентиированный граф, в котором вершины представляют собой типы
(домены), а дуги предсталяют собой функции (морфизмы) переводящие значения
исходных типов в значения выходных типов. Такая программа (категория) обычно
называется модулями. Сам модуль может содержать функции, другие типы другие
модули (категории как типы), т.е. содержит типы и значения (значения обычно
являются функциями). Для конструкции других типов можно применять все описанные
выше конструкторы типов. Конструкторы типов product и sum определяют так
называемые алгебраические типы данных, с помощью которых можно строить сложные
типы:

tree(A) = sum(product(A),product(tree(A),tree(A))) = {A} | {tree(A),tree(A)}.
array(T) = list(list(T)).
cube(T) = list(array(T)).
typeCons(A,B,C) = product(sum(A,B),list(C)) = {A | B,list(C)}.

Сам тип конструкторов типов можно определить псевдо-сигнатурой алгебраического
типа sum(fun,...):

type/Arity = product/Arity | sum/Arity | fun/Arity | cat/Arity | list/1 | any/0.

Если у конструктора есть параметры которые неизвестны это означает что этот
конструктор определяет целый класс типов, т.е. является функцией от других
типов. Например:

typeCons = product(any(),any(),list/1).
main = fun/2.
product/3 = product(any(),any(),any()).
mylist = product(list(product/3),sum/2,any()).
lst = list/1.
functorArg = type/1.

Могут быть типы c частичной параметризацией всех своих параметров:

mixed(T,A) = product(A,any(),sum(T,list(T)),product/3,fun/2,functor(list/1)).

Как видите mixed(T,A) практически неотличим от Эрланг фунции, что является
очевидным и наглядным предствляем лямбда исчисления второго порядка над
полиморфными типами.

Функции

Функции относятся к лямбда исчисления первого порядка определенному на значения
некоторых типов. Диалайзера синтаксис сигнатуры типа-функции определяется так:

fun((A,B,...)->C).

Я предлагаю упростить его до

fun(A,B,...,C).

где посладний параметр в конструкторе типа это тип возвращаемого значения или
вовсе он не указывается.

Вот например как могла бы выглядеть функция fmap с типизированной вручную
сигнатурой:

listmap = fun((Fun::fun(A::X,B::Y),In::list(X))->list(Y)) ->
    io:format("In: ~p",[In]),
    Out = [ Fun(E) || E <- In],
    io:format("Out: ~p",[Out]),
    Out end.

Другие примеры задания сигнатур с помощью конструкторов:

fmap = fun(fun(any,any),list/1).
listmap = fun(fun(A,B),list(A),list(B)).
unimap(A,B,T::type/1) = fun(fun(A,B),T(A),T(B)).

В Haskell конструкторы типов пишутся с большой буквы (потому что Λ -- уровень
типов), а функции пишутся с маленькой (потому что λ -- уровень значений), но в
Эрланге исторически так сложилось что именно переменные типов пишутся с большой
а сами типы пишутся с маленькой + ко всем функции еще пишутся с маленькой
поэтому в нашем языке будет маленькая неразбериха для совместимости с
существующим Эрланг кодом.

a = tree(integer()).
B = {1}.

Исключения только для биндингов где сразу указано значение типа (с маленькой
тогда буквы).

b = tree(integer()) -> {1}.
join = fun(A,B) -> lists:join(A,B) end.

Модули

Модули являются типами верхнего уровня, в которые запаковываются другие типы и
значения (обычно функций, т.е. тела функций).

Functor = cat(Type::type/1) -> fmap = fun(fun(A,B),Type(A),Type(B)). end.

Экземпляр такого типа можно задать параметризировав такой тип и указав тело:

Listfunctor = Functor(list/1) -> fmap(F,X) -> listmap(F,X). end.

После этого инстанс готов к употреблению:

Square = fun(X) -> X * X end.
Listfunctor:fmap(Square,[1,2,3,4]).

Или например этот же модуль Функтор можно использовать для деревьев:

TreeFunctor = Functor(tree/1) ->
    fmap(F,{X}) -> { F(X) };
    fmap(F,{L,R}) -> { fmap(F,{L}), fmap(F,{R}) }. end.

Волшебным образом эрланговский код стал типизированным :)

Всем кто дочитал до этого места, спасибо за внимание.